package CTL;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.LinkedList;

import systeme.GrapheRdP;

public class CTLArriere {
	
	GrapheRdP grapheRdp ;


	public CTLArriere(GrapheRdP graphe){
		
		this.grapheRdp = graphe ;
		
	}
  

    public boolean[] prop(int place) {
    	
    	boolean[] res = new boolean[grapheRdp.nbEtat];
    	for (int i = 0 ; i < grapheRdp.nbEtat ; i++){
    		
    		res[i] = grapheRdp.etat.get(i)[place];
    	}
    	
    	return res;
    	
    }

    public boolean[] faux() {
	boolean[] res = new boolean[grapheRdp.succ.size()];
	Arrays.fill(res,false);
	return res;
    }

    public boolean[] vrai() {
	boolean[] res = new boolean[grapheRdp.succ.size()];
	Arrays.fill(res,true);
	return res;
    }

    public boolean[] neg(boolean[] a) {
    int taille = grapheRdp.succ.size() ;
	boolean[] res = new boolean[taille];
	for (int i=0; i<taille; i++)
	    res[i] = !a[i];
	return res;
    }
   
    public boolean[] or(boolean[] a, boolean[] b) {
    	int taille = grapheRdp.succ.size();
	boolean[] res = new boolean[taille];
	for (int i=0; i<taille; i++)
	    res[i] = a[i] || b[i];
	return res;
    }

    public boolean[] and(boolean[] a, boolean[] b) {
    	
    int taille = grapheRdp.succ.size();
	boolean[] res = new boolean[taille];
	for (int i=0; i<taille; i++)
	    res[i] = a[i] && b[i];
	return res;
    }

    /*
     * @param a  : liste des prorietes a verifie 
     */
    public boolean[] EX(boolean[] a) {
    
    	// //taille => nombre de place
    	int taille = grapheRdp.pred.size();
    	//res = empty
    	boolean[] res = new boolean[taille];
    	
    	//parcourir les etats
    	for (int i=0; i<taille; i++) {
    		res[i] = false;
    		//pour tout etat verifiant la propriété => ajout a res des predecesseur
    		if(a[i])
    		{
    			//ajout des preds
    			for(int j=0;j<grapheRdp.recupererPred(i).size();j++)
    				res[grapheRdp.recupererPred(i).get(j)] = true;
    		}
    	}
    	/*
    	String aff = new String();
    	aff+="EX res : ";
    	for(int i=0;i<taille;i++)
    		aff+= res[i];
    	aff+="\n";
    	System.out.println(aff);*/
    	return res;
    }

    public boolean[] AX(boolean[] a) {
    	return neg(EX(neg(a)));
    } 

    public boolean[] EU(boolean[] a, boolean[] b) 
    {
    	boolean[] res = faux();
    	LinkedList<Integer> todo = new LinkedList<Integer>();

    	//parcourir les places et ajouter a res&todo ceux qui verifie b
    	for(int i=0;i<grapheRdp.pred.size();i++)
    	{
    		if(b[i])
    		{
    			res[i] = true;
    			todo.addLast(i);
    		}
    	}

    	//pour chaque etat dans todo
    	while(todo.size()!=0)
    	{
    		//on retire l'etat courant (en tete)
    		int s=todo.removeFirst();
    		//tmp recois tout les predecesseur verifiant f n'etant pas deja dans res
    		ArrayList<Integer> tmp = new ArrayList<Integer>();
    		//parcours des preds
    		for(int i=0;i<grapheRdp.recupererPred(s).size();i++)
    		{
    			int pred =grapheRdp.recupererPred(s).get(i); 
    			//le pred verifie a sans etre dans res
    			if(!res[pred] && a[pred])
    				tmp.add(pred);
    		}
    		/*
    		 * todo = todo union tmp
    		 * res = res union tmp 
    		*/
    		for(int i=0;i<tmp.size();i++)
    		{
    			todo.addLast(tmp.get(i));
    			res[tmp.get(i)] = true;
    		}
    	}
    	
    	String aff = new String();
    	aff+="EX res : ";
    	for(int i=0;i<res.length;i++)
    		aff+= res[i];
    	aff+="\n";
    	System.out.println(aff);
    	
    	return res;
    }

    public boolean[] AU(boolean[] a, boolean[] b) {
	boolean[] res = faux();
	boolean[] avant;
	do {
	    avant = res;
	    res = or(b,and(a,AX(res)));
	} 
	while(!Arrays.equals(avant,res));
	return res;
    }
}